CBMC
dfcc_check_loop_normal_form.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for loop contracts
4 
5 Author: Qinheping Hu, qinhh@amazon.com
6 Author: Remi Delmas, delmasrd@amazon.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CHECK_LOOP_NORMAL_FORM_H
14 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CHECK_LOOP_NORMAL_FORM_H
15 
16 class goto_programt;
17 class messaget;
18 
47 void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log);
48 
49 #endif
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
dfcc_check_loop_normal_form
void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log)
Checks and enforces normal form properties for natural loops of the given goto_program.
Definition: dfcc_check_loop_normal_form.cpp:15
log
double log(double x)
Definition: math.c:2776