Loading...

Searching...

No Matches

race_check.h

Go to the documentation of this file.

1/*******************************************************************\

2

3Module: Race Detection for Threaded Goto Programs

4

5Author: Daniel Kroening

6

7Date: February 2006

8

9\*******************************************************************/

10

13

14#ifndef CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H

15#define CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H

16

17#ifdef LOCAL_MAY

18# include <goto-programs/goto_functions.h>

19#endif

20

21#include <util/irep.h>

22

23class goto_modelt;

24class goto_programt;

25class message_handlert;

26class value_setst;

27

28void race_check(

29 value_setst &,

30 class symbol_table_baset &,

31 const irep_idt &function_id,

32#ifdef LOCAL_MAY

33 const goto_functionst::goto_functiont &goto_function,

34#endif

35 goto_programt &goto_program,

36 message_handlert &);

37

38void race_check(value_setst &, goto_modelt &, message_handlert &);

39

40#endif // CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

dstringt

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

goto_functionst::goto_functiont

::goto_functiont goto_functiont

Definition goto_functions.h:27

goto_modelt

Definition goto_model.h:27

goto_programt

A generic container class for the GOTO intermediate representation of one function.

Definition goto_program.h:72

message_handlert

Definition message.h:27

symbol_table_baset

The symbol table base class interface.

Definition symbol_table_base.h:23

value_setst

Definition value_sets.h:22

goto_functions.h

Goto Programs with Functions.

irep.h

race_check

void race_check(value_setst &, class symbol_table_baset &, const irep_idt &function_id, goto_programt &goto_program, message_handlert &)

Definition race_check.cpp:269

CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/race_check.h Source File