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 021ebd9 commit a9c7f8cCopy full SHA for a9c7f8c
regression/cbmc-cover/branch-loop1/main.c
@@ -0,0 +1,11 @@
1
+int main(int argc, char **argv)
2
+{
3
+ for(int i = 0; i < 4; i++)
4
+ {
5
+ char c;
6
+ __CPROVER_input("c", c);
7
+ if(c == 42)
8
+ return 0;
9
+ }
10
+ return 1;
11
+}
regression/cbmc-cover/branch-loop1/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--xml-ui --cover branch
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+</inputs>\n\s*<goal id="main\.coverage\.1"/>\n\s*<goal id="main\.coverage\.2"/>\n\s*<goal id="main\.coverage\.3"/>\n\s*<goal id="main\.coverage\.5"/>\n\s*</test>
+
+--
+^warning: ignoring
12
+Expect each goal only occur once per test.
0 commit comments