CBMC
character_refine_preprocess.h File Reference

Preprocess a goto-programs so that calls to the java Character library are replaced by simple expressions. More...

#include <util/mp_arith.h>
#include <util/std_code_base.h>
#include <list>
#include <unordered_map>
+ Include dependency graph for character_refine_preprocess.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  character_refine_preprocesst
 

Detailed Description

Preprocess a goto-programs so that calls to the java Character library are replaced by simple expressions.

For now support is limited to character in the ASCII range, some methods may have incorrect specifications outside of this range.

Definition in file character_refine_preprocess.h.