From 46f62314e6d48089fb646fac3a776d45f27f865e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 26 May 2018 09:46:44 +0100 Subject: [PATCH] cbmc test no longer uses --cover --- .../regenerate-entry-function/main.c | 20 ++++--------------- .../regenerate-entry-function/test.desc | 6 +++--- 2 files changed, 7 insertions(+), 19 deletions(-) diff --git a/regression/goto-cc-cbmc/regenerate-entry-function/main.c b/regression/goto-cc-cbmc/regenerate-entry-function/main.c index 644ef1eb086..cdde8631a7c 100644 --- a/regression/goto-cc-cbmc/regenerate-entry-function/main.c +++ b/regression/goto-cc-cbmc/regenerate-entry-function/main.c @@ -1,23 +1,11 @@ +#include + int fun(int x) { - if(x > 0) - { - return x * x; - } - else - { - return x; - } + assert(0); } int main(int argc, char** argv) { - if(argc>4) - { - return 0; - } - else - { - return 1; - } + return 0; } diff --git a/regression/goto-cc-cbmc/regenerate-entry-function/test.desc b/regression/goto-cc-cbmc/regenerate-entry-function/test.desc index 1ee374f196c..4735941b0f0 100644 --- a/regression/goto-cc-cbmc/regenerate-entry-function/test.desc +++ b/regression/goto-cc-cbmc/regenerate-entry-function/test.desc @@ -1,8 +1,8 @@ CORE main.c -'--function fun --cover branch' -^EXIT=0$ +'--function fun' +^EXIT=10$ ^SIGNAL=0$ -^x= +^VERIFICATION FAILED$ -- ^warning: ignoring