search

CSU-CS-Melange / AlphaZ

MIT License
1 stars 0 forks source link

External function verification fix #3

Closed lnarmour closed 1 year ago

lnarmour commented 1 year ago

Fixes issue #1. When external functions are used, the code generator creates an associated header file (called external_functions.h. The user is subsequently supposed to define these functions in that header file. See here, for example:
https://www.cs.colostate.edu/AlphaZ/wiki/doku.php?id=tutorial_external_function

However, when generateVerificationCode is called in the presence of external functions, the verification code also includes this same header (and subsequently the same definitions), and throws errors like this when trying to make:

$ make verify
cc bug.c -o bug.o -O3  -std=c99  -I/usr/include/malloc/ -lm -c
clang: warning: -lm: 'linker' input unused [-Wunused-command-line-argument]
cc bug_verify.c -o bug_verify.o -O3  -std=c99  -I/usr/include/malloc/ -lm -c
clang: warning: -lm: 'linker' input unused [-Wunused-command-line-argument]
cc bug-wrapper.c -o bug.verify bug.o  bug_verify.o -O3  -std=c99  -I/usr/include/malloc/ -lm -DVERIFY
duplicate symbol '_userfunc' in:
    bug.o
    bug_verify.o
ld: 1 duplicate symbol for architecture arm64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [verify] Error 1

Now, the verification codegen only generates the external function declarations in the ***_verify.c file.