CBMC
Loading...
Searching...
No Matches
dfcc_check_loop_normal_form.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for loop contracts
4
5Author: Qinheping Hu, qinhh@amazon.com
6Author: 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
16class goto_programt;
17class messaget;
18
47void 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:72
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:2449