CBMC
expr2java.h File Reference
#include <cmath>
#include <sstream>
#include <string>
#include <ansi-c/expr2c_class.h>
+ Include dependency graph for expr2java.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  expr2javat
 

Functions

std::string expr2java (const exprt &expr, const namespacet &ns)
 
std::string type2java (const typet &type, const namespacet &ns)
 
template<typename float_type >
std::string floating_point_to_java_string (float_type value)
 Convert floating point number to a string without printing unnecessary zeros. More...
 

Function Documentation

◆ expr2java()

std::string expr2java ( const exprt expr,
const namespacet ns 
)

Definition at line 454 of file expr2java.cpp.

◆ floating_point_to_java_string()

template<typename float_type >
std::string floating_point_to_java_string ( float_type  value)

Convert floating point number to a string without printing unnecessary zeros.

Prints decimal if precision is not lost. Prints hexadecimal otherwise, and/or java-friendly NaN and Infinity

Definition at line 60 of file expr2java.h.

◆ type2java()

std::string type2java ( const typet type,
const namespacet ns 
)

Definition at line 461 of file expr2java.cpp.