cprover
java_bytecode_typecheck_expr.cpp File Reference

JAVA Bytecode Conversion / Type Checking. More...

#include "java_bytecode_typecheck.h"
#include <iomanip>
#include <util/std_expr.h>
#include <util/prefix.h>
#include <util/arith_tools.h>
#include <util/unicode.h>
#include <linking/zero_initializer.h>
#include "java_pointer_casts.h"
#include "java_types.h"
Include dependency graph for java_bytecode_typecheck_expr.cpp:

Go to the source code of this file.

Functions

static std::string escape_non_alnum (const std::string &toescape)
 
static array_exprt utf16_to_array (const std::wstring &in)
 Convert UCS-2 or UTF-16 to an array expression. More...
 

Detailed Description

JAVA Bytecode Conversion / Type Checking.

Definition in file java_bytecode_typecheck_expr.cpp.

Function Documentation

◆ escape_non_alnum()

static std::string escape_non_alnum ( const std::string &  toescape)
static

◆ utf16_to_array()

static array_exprt utf16_to_array ( const std::wstring &  in)
static

Convert UCS-2 or UTF-16 to an array expression.

parameters: in: wide string to convert
Returns
Returns a Java char array containing the same wchars.

Definition at line 91 of file java_bytecode_typecheck_expr.cpp.

References exprt::copy_to_operands(), from_integer(), java_char_type(), and java_int_type().

Referenced by java_bytecode_typecheckt::typecheck_expr_java_string_literal().