From f57b3d0a8c83c2fd328ffcc1dc8d7641175021b9 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 8 Feb 2021 17:03:24 +0100
Subject: [PATCH] [tests] add extra check related to logic preprocessing
---
tests/jcdb/logic-pp-include/no-stdio.c | 2 ++
tests/jcdb/oracle/logic-pp-include.res | 1 +
2 files changed, 3 insertions(+)
diff --git a/tests/jcdb/logic-pp-include/no-stdio.c b/tests/jcdb/logic-pp-include/no-stdio.c
index 78444816bb2..5dfc21439f0 100644
--- a/tests/jcdb/logic-pp-include/no-stdio.c
+++ b/tests/jcdb/logic-pp-include/no-stdio.c
@@ -1,4 +1,6 @@
// compile_commands.json must have "-includestdio.h" and define ZERO
+
+//@ ensures \result == ZERO;
int main(){
printf("bla\n");
return ZERO;
diff --git a/tests/jcdb/oracle/logic-pp-include.res b/tests/jcdb/oracle/logic-pp-include.res
index a6aedf5c3dd..a8432079471 100644
--- a/tests/jcdb/oracle/logic-pp-include.res
+++ b/tests/jcdb/oracle/logic-pp-include.res
@@ -4,6 +4,7 @@
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
+/*@ ensures \result ≡ 0; */
int main(void)
{
int __retres;
--
GitLab