#include <goto-programs/goto_functions.h>
#include <transition-system/transition_system.h>
#include <util/config/options.h>
#include <util/symtab/context.h>
#include <string>

Include dependency graph for ts_extraction.h:

This graph shows which files directly or indirectly include this file:

Functions
bool	extract_transition_system (const goto_functionst &goto_functions, contextt &context, const optionst &options, transition_systemt &ts)
	Recognise a single unbounded loop in main (after the k-induction transformation) and extract it into ts, running symbolic execution over one iteration.

Function Documentation

◆ extract_transition_system()

bool extract_transition_system	(	const goto_functionst &	goto_functions,
		contextt &	context,
		const optionst &	options,
		transition_systemt &	ts )

Recognise a single unbounded loop in main (after the k-induction transformation) and extract it into ts, running symbolic execution over one iteration.

Returns whether the operation succeded.

For

unsigned char x = 0;
for (;;) { __ESBMC_assert(x < 4, "range"); x = (x + 1) & 3; }

symex of one iteration gives (SSA names shortened):

x@1 == 0               prefix
x@2 == nondet          the havoc: state at the loop head
guard => x@2 < 4       the claim
x@3 == (x@2 + 1) & 3   the body's assignment

which is carved into

states[0]   name "x", init 0, pre x@2, post x@3
body_defs   x@3 == (x@2 + 1) & 3
bad[0]      x@2 >= 4
back_guard  true

Recognise a single unbounded loop in main (after the k-induction transformation) and extract it into ts, running symbolic execution over one iteration.

x = 0                 prefix
ts$init$0 = x         <- before the havoc: value entering the loop
x = nondet()             the k-induction havoc

head: ts$pre$0 = x <- before the head: state at the loop head assert(x < 4) body x = (x + 1) & 3 ts$post$0 = x <- before the back edge: state at the back edge goto head

One symbolic execution of that yields an SSA in which the marker assignments cut everything into regions:

x@1 == 0              i < init_first        -> prefix_defs
ts$init$0 == x@1      init_first            -> states[0].init
x@2 == nondet         havoc region             dropped (is_only)
ts$pre$0 == x@2       pre_first..pre_last   -> states[0].pre
guard => x@2 < 4      i > pre_last          -> bad
x@3 == (x@2 + 1) & 3                        -> body_defs
ts$post$0 == x@3      post_first            -> states[0].post

So each marker's rhs is the value wanted, and the steps between markers are the prefix and the body: assignments become *_defs, assumes become *_assumes (or invariants when inductive-step-only), asserts become *_bad. back_guard is the guard the first ts$post$ step carries.

Functions

Function Documentation

◆ extract_transition_system()