We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 62880cd commit b1be232Copy full SHA for b1be232
regression/cbmc-primitives/r_w_ok_bug/main.c
@@ -0,0 +1,9 @@
1
+#include <assert.h>
2
+#include <stdlib.h>
3
+
4
+void main()
5
+{
6
+ char *p1;
7
+ __CPROVER_assume(__CPROVER_r_ok(p1 - 1, 1));
8
+ *p1;
9
+}
regression/cbmc-primitives/r_w_ok_bug/test.desc
+KNOWNBUG
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+Crashes during the flattening, issue #5328
0 commit comments