Skip to content
Snippets Groups Projects
Commit f57b3d0a authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[tests] add extra check related to logic preprocessing

parent 9170a765
No related branches found
No related tags found
No related merge requests found
// compile_commands.json must have "-includestdio.h" and define ZERO // compile_commands.json must have "-includestdio.h" and define ZERO
//@ ensures \result == ZERO;
int main(){ int main(){
printf("bla\n"); printf("bla\n");
return ZERO; return ZERO;
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
#include "stdarg.h" #include "stdarg.h"
#include "stddef.h" #include "stddef.h"
#include "stdio.h" #include "stdio.h"
/*@ ensures \result ≡ 0; */
int main(void) int main(void)
{ {
int __retres; int __retres;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment