From 92ceae3cf62df73a4ec96251a6af09552fd86ce5 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Thu, 18 Jun 2015 16:09:14 -0200 Subject: [PATCH] [clang frontend] Fix translation of large integer constants. --- infer/src/clang/cTrans.ml | 24 +++++++++++++------ .../c/frontend/arithmetic/int_const.c | 4 ++++ .../c/frontend/arithmetic/int_const.dot | 16 +++++++++---- 3 files changed, 33 insertions(+), 11 deletions(-) diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index a82389a0f..526850d7d 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -219,12 +219,20 @@ struct and integerLiteral_trans trans_state stmt_info expr_info integer_literal_info = Printing.log_out "Passing from IntegerLiteral '%s'\n" stmt_info.Clang_ast_t.si_pointer; let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.tenv in - let i = try - int_of_string (integer_literal_info.Clang_ast_t.ili_value) - with _ -> (Random.int 10000) +1 in - let exp = Sil.Const (Sil.Cint (Sil.Int.of_int i)) in - (* In case of overflow we return a random number. To avoid 0 we add plus one.*) - { empty_res_trans with exps = [(exp, typ)]} + let exp, ids = + try + let i = Int64.of_string integer_literal_info.Clang_ast_t.ili_value in + let exp = Sil.exp_int (Sil.Int.of_int64 i) in + exp, [] + with + | Failure _ -> + (* Parse error: return a nondeterministic value *) + let id = Ident.create_fresh Ident.knormal in + let exp = Sil.Var id in + exp, [id] in + { empty_res_trans with + exps = [(exp, typ)]; + ids = ids; } let nullStmt_trans succ_nodes stmt_info = Printing.log_out "Passing from NullStmt '%s'.\n" stmt_info.Clang_ast_t.si_pointer; @@ -1786,7 +1794,9 @@ struct (match stmts with | [stmt1; ostmt1; ostmt2; stmt2] when contains_opaque_value_expr ostmt1 && contains_opaque_value_expr ostmt2 -> conditionalOperator_trans trans_state stmt_info [stmt1; stmt1; stmt2] expr_info - | _ -> Printing.log_stats "BinaryConditionalOperator not translated %s @." (Ast_utils.string_of_stmt instr); + | _ -> Printing.log_stats + "BinaryConditionalOperator not translated %s @." + (Ast_utils.string_of_stmt instr); assert false) | s -> (Printing.log_stats "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: Translation need to be defined. Statement ignored.... \n" diff --git a/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.c b/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.c index e0c5ba0be..55bcb3779 100644 --- a/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.c +++ b/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.c @@ -11,5 +11,9 @@ float *const c; long double d; static const int kDuration = 3; + + int large_int = 9223372036854775807; + int overflow_int = 9223372036854775808; + return 0; } diff --git a/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.dot b/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.dot index db3d9af13..5584874d0 100644 --- a/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.dot +++ b/infer/tests/codetoanalyze/c/frontend/arithmetic/int_const.dot @@ -1,17 +1,25 @@ digraph iCFG { -4 [label="4: DeclStmt \n *&#GB$main_kDuration:int =3 [line 13]\n " shape="box"] +6 [label="6: DeclStmt \n *&#GB$main_kDuration:int =3 [line 13]\n " shape="box"] + + + 6 -> 5 ; +5 [label="5: DeclStmt \n *&large_int:int =9223372036854775807 [line 15]\n NULLIFY(&large_int,false); [line 15]\n " shape="box"] + + + 5 -> 4 ; +4 [label="4: DeclStmt \n *&overflow_int:int =n$0 [line 16]\n REMOVE_TEMPS(n$0); [line 16]\n NULLIFY(&overflow_int,false); [line 16]\n " shape="box"] 4 -> 3 ; -3 [label="3: Return Stmt \n *&return:int =0 [line 14]\n APPLY_ABSTRACTION; [line 14]\n " shape="box"] +3 [label="3: Return Stmt \n *&return:int =0 [line 18]\n APPLY_ABSTRACTION; [line 18]\n " shape="box"] 3 -> 2 ; 2 [label="2: Exit main \n " color=yellow style=filled] -1 [label="1: Start main\nFormals: \nLocals: a:int b:int * c:float * d:long double \n DECLARE_LOCALS(&return,&a,&b,&c,&d); [line 6]\n NULLIFY(&a,false); [line 6]\n NULLIFY(&b,false); [line 6]\n NULLIFY(&c,false); [line 6]\n NULLIFY(&d,false); [line 6]\n " color=yellow style=filled] +1 [label="1: Start main\nFormals: \nLocals: a:int b:int * c:float * d:long double large_int:int overflow_int:int \n DECLARE_LOCALS(&return,&a,&b,&c,&d,&large_int,&overflow_int); [line 6]\n NULLIFY(&a,false); [line 6]\n NULLIFY(&b,false); [line 6]\n NULLIFY(&c,false); [line 6]\n NULLIFY(&d,false); [line 6]\n NULLIFY(&large_int,false); [line 6]\n NULLIFY(&overflow_int,false); [line 6]\n " color=yellow style=filled] - 1 -> 4 ; + 1 -> 6 ; }