Output of the program (SSA) constraints. More...
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Functions | |
| void | show_program (const namespacet &ns, const symex_target_equationt &equation) |
Print the steps of equation on the standard output. More... | |
| void | show_byte_ops (const optionst &options, ui_message_handlert &ui_message_handler, const namespacet &ns, const symex_target_equationt &equation) |
| Count and display all byte extract and byte update operations from equation on standard output or file. More... | |
Detailed Description
Output of the program (SSA) constraints.
Definition in file show_program.h.
Function Documentation
◆ show_byte_ops()
| void show_byte_ops | ( | const optionst & | options, |
| ui_message_handlert & | ui_message_handler, | ||
| const namespacet & | ns, | ||
| const symex_target_equationt & | equation | ||
| ) |
Count and display all byte extract and byte update operations from equation on standard output or file.
The name of the output file is given by the outfile option from options, the standard output is used if it is not provided. The format is either JSON or plain text depending on ui_message_handler; XML is not supported. For each step, if it's a byte extract or update, print location, ssa expression and compute number of extracts/updates in total in the equation.
- Parameters
-
options parsed options ui_message_handler ui message handler ns namespace equation SSA form of the program
Definition at line 322 of file show_program.cpp.
◆ show_program()
| void show_program | ( | const namespacet & | ns, |
| const symex_target_equationt & | equation | ||
| ) |
Print the steps of equation on the standard output.
For each step, prints the location, then if the step is an assignment, assertion, assume, constraint, shared read or shared write: prints an instruction counter, followed by the instruction type, and the current guard if it is not equal to true.
- Parameters
-
ns namespace equation SSA form of the program
Definition at line 60 of file show_program.cpp.
