[C] Incorrect "Verification successful" for k-induction when utilizing goto's

[XaverFink]

I'm using ESBMC for a case study and am getting a false positive with the k-induction feature. With plain BMC without k-induction ESBMC manages to find the counterexample. I broke down the program to a minimal example as seen below. I added comments noting what changes in the minimal example lead to the counterexample being found.

To me it looks like it might be caused by incorrect handling of the goto-statements. Is this a known bug?

This bug was found on the newest ESBMC 7.5 release on a Windows 11 machine with the command .\bin\esbmc.exe .\minimal_example.c --k-induction.

#include <stdbool.h>

// Variables
bool isFirstCycle = true;
bool property = true;

// Main
void main() {
	goto loop_start;
	loop_start: {
		goto monitor_evaluation;
	}
	
	property_check: {
		// Does not find the violation
		__ESBMC_assert(property, "assertion error");
		goto loop_start;	
	}
		
	monitor_evaluation: {
		// Property becomes false at second iteration
		property = (isFirstCycle ? (true) : (false)) ;
		isFirstCycle = false;
		// Violation found if uncommented
		//__ESBMC_assert(property, "assertion error");
		goto property_check;	
	}
	
	/* If we put the property_check under the monitor_evaluation the violation is also found
	property_check: {
		// Violation found
		__ESBMC_assert(property, "assertion error");
		goto loop_start;	
	}
	*/
	return;
}

[mikhailramalho]

Reduced test case:

_Bool a = 1;
_Bool b = 0;

int main() {
  goto c;
d:
  __ESBMC_assert(b, "");
c:
  b = a;
  a = 0;
  goto d;
}

the k-induction transformations don't identify the loop so no variable is set to nondet in label d:

main (c:@F@main):
        // 20 file main.c line 5 column 3 function main
        GOTO 2
        // 21 file main.c line 7 column 3 function main
     1: ASSERT b
        // 22 file main.c line 9 column 3 function main
        // Labels: c
     2: b=a;
        // 23 file main.c line 10 column 3 function main
        a=0;
        // 24 file main.c line 11 column 3 function main
        GOTO 1
        // 25 file main.c line 12 column 1 function main
        END_FUNCTION // main

[mikhailramalho]

it looks like esbmc finds the loop tho:

$ esbmc main.c --show-loops
ESBMC version 7.5.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing main.c
Converting
Generating GOTO Program
GOTO program creation time: 0.443s
GOTO program processing time: 0.000s
goto-loop Loop 1:
 file stdlib.c line 36 column 3 function __ESBMC_atexit_handler

goto-loop Loop 2:
 file main.c line 11 column 3 function main

[ChenfengWei0]

This issue can be avoided, to some extent, by using --k-step = num.

esbmc file.c --k-induction

Checking inductive step, k = 2
Starting Bounded Model Checking
Unwinding loop 3 iteration 1   file file.c line 26 column 3 function main
Unwinding loop 2 iteration 1   file file.c line 17 column 3 function main
Not unwinding loop 3 iteration 2   file file.c line 26 column 3 function main
Symex completed in: 0.000s (16 assignments)
Slicing time: 0.000s (removed 15 assignments)
Generated 1 VCC(s), 0 remaining after simplification (1 assignments)
BMC program time: 0.000s

VERIFICATION SUCCESSFUL

Solution found by the inductive step (k =2)

esbmc file.c --k-induction --k-step 2

Checking base case, k = 3
Starting Bounded Model Checking
Unwinding loop 3 iteration 1   file file.c line 26 column 3 function main
Unwinding loop 2 iteration 1   file file.c line 17 column 3 function main
Unwinding loop 3 iteration 2   file file.c line 26 column 3 function main
Unwinding loop 2 iteration 1   file file.c line 17 column 3 function main
Not unwinding loop 3 iteration 3   file file.c line 26 column 3 function main
Symex completed in: 0.001s (20 assignments)
Slicing time: 0.000s (removed 17 assignments)
Generated 2 VCC(s), 1 remaining after simplification (3 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
Building error trace

[Counterexample]


State 1 file file.c line 16 column 3 function main thread 0
----------------------------------------------------
Violated property:
  file file.c line 16 column 3 function main
  assertion error
  (_Bool)property


VERIFICATION FAILED

Bug found (k = 3)

---

This issue #1092 might be related