Skip to content

--add-library on 32 bit code seems to use 64 bit library #2949

Closed
@markrtuttle

Description

@markrtuttle

With the file main.c

#include <string.h>

int main(){
  char buffer[] = "a";
  int x = strlen(buffer);
  return x;
}

the commands

goto-cc -m32 -o main.gb main.c
goto-instrument --add-library main.gb main2.gb

report numerous conflicts including

file <builtin-architecture-strings> line 3: warning: conflicting initializers for variable "__CPROVER_architecture_long_int_width"
using old value in module main file <builtin-architecture-strings> line 3
32
ignoring new value in module <built-in-library> file <builtin-architecture-strings> line 3
64

I can see from the symbol table that something has been added (strlen::1::len and strlen::s), but I'm not sure I can trust the result. I don't see the equivalent of --32 or -m32 for goto-instrument (it doesn't recognize these flags). I tried to submit this as a KNOWNBUG test case for goto-instrument, but couldn't see how to write a test.desc that would pass -m32 to cbmc before running goto-instrument.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions