cbmc-starter-kit
cbmc-starter-kit copied to clipboard
model-checking
Makefile silent when addone function doesn't exist
When addone function is not defined but used in UNWINDSET like below:
UNWINDSET += somefunction.0:$(call addone,$(SOME_LEN))
The Makefile won't generate an error, instead I observe that the proof will not terminate. I'm guessing it is because the unwinding level is treated as infinite and CBMC just keeps unwinding the loop.
It will be nicer if an error is generated saying addone is not defined. Or another fix is to add the addone definition into the Makefiles generated by cbmc-started-kit, since it is probably needed for loop unwinding proofs.
We could ponder adding MAKEFLAGS=--warn-undefined-variables to Makefile.common, but I'm not sure whether this would break anything. (Perhaps you could give make --warn-undefined-variables a try, which accomplishes the same, just on the command line?)
I tried make --warn-undefined-variables with both addone defined and not defined. In the case addone is defined, the proof is successful. In the case it is not defined, I do get several warnings about undefined variable addone. So it seems like adding that flag won't break anything (in the single case I tried).
The only problem is that, the output is not user friendly. First there already exists variables in Makefile.common that are not defined, so those get reported too. Second, each occurrence of an undefined variable gets a warning. So I got a ton of repeated ones.
What is addone? Is this a Makefile macro that you would like to define? A reasonable place to put this definition would be in the Makefile-project-defines.
It's a macro used in e.g. ESDK-C
Defined here: https://github.com/aws/aws-encryption-sdk-c/blob/2743a977b3959e23131903b1a70dbc4749632a5f/verification/cbmc/proofs/Makefile.local_default#L23
Used e.g. here: https://github.com/aws/aws-encryption-sdk-c/blob/2743a977b3959e23131903b1a70dbc4749632a5f/verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/Makefile#L64
Let's use this as an example in the training material of something that would be useful to add to the makefile project defines.
