Closed
Description
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
Labels
No labels