Skip to content

Commit

Permalink
Fix trailing whitespace and newlines
Browse files Browse the repository at this point in the history
  • Loading branch information
reb-ddm committed Jan 4, 2024
1 parent 46802dd commit 5f56257
Show file tree
Hide file tree
Showing 13 changed files with 173 additions and 175 deletions.
2 changes: 1 addition & 1 deletion src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -32,5 +32,5 @@ let after_config () =
MCP.register_analysis (module Spec : MCPSpec);
GobConfig.set_string "ana.path_sens[+]" (Spec.name ())

let _ =
let _ =
AfterConfig.register after_config
319 changes: 159 additions & 160 deletions src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions src/cdomains/apron/sharedFunctions.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -477,7 +477,7 @@ end

(* Multi-precision rational numbers, defined by Apron.
Used by affineEqualityDomain and linearTwoVarEqualityDomain *)
module Mpqf = struct
module Mpqf = struct
include Mpqf
let compare = cmp
let zero = of_int 0
Expand Down Expand Up @@ -512,7 +512,7 @@ module BoundsCheckMeetTcons (Bounds: ExtendedConvBounds) (V: SV) = struct
| Some v ->
let ik = Cilfacade.get_ikind v.vtype in
match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res (Bounds.get_env res) (Lval (Cil.var v)) true) with
| Some _, Some _ when not (Cil.isSigned ik) -> raise NotRefinable
| Some _, Some _ when not (Cil.isSigned ik) -> raise NotRefinable
| Some min, Some max ->
assert (Z.equal min max); (* other bounds impossible in affeq *)
let (min_ik, max_ik) = IntDomain.Size.range ik in
Expand All @@ -521,4 +521,4 @@ module BoundsCheckMeetTcons (Bounds: ExtendedConvBounds) (V: SV) = struct
else res
| exception Convert.Unsupported_CilExp _
| _, _ -> overflow_res res
end
end
1 change: 0 additions & 1 deletion tests/regression/77-lin2vareq/00-basic.c
Original file line number Diff line number Diff line change
Expand Up @@ -19,4 +19,3 @@ int main() {

return 0;
}

2 changes: 1 addition & 1 deletion tests/regression/77-lin2vareq/01-iteration.c
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,4 @@ int main() {
return 0;
}

//This test case checks whether the value of variable i is always equal to the value of variable j within the loop.
//This test case checks whether the value of variable i is always equal to the value of variable j within the loop.
2 changes: 1 addition & 1 deletion tests/regression/77-lin2vareq/02-reachability.c
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ int main() {
y = 1;

__goblint_check(x == 10 * y); //SUCCESS

if(x == 10 * y)
return 0;
__goblint_check(0); // NOWARN (unreachable)
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/77-lin2vareq/03-known_expressions.c
Original file line number Diff line number Diff line change
Expand Up @@ -23,4 +23,4 @@ int main() {
__goblint_check(x12 == 2 * x11 + 1); //SUCCESS

return 0;
}
}
4 changes: 2 additions & 2 deletions tests/regression/77-lin2vareq/04-unknown.c
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
#include <stdio.h>

typedef int dataX_t;
typedef int dataY_t;
typedef int dataY_t;

dataX_t x_arr[100];
dataY_t y_arr[100];
Expand All @@ -23,7 +23,7 @@ int main() {

for (i = 0; i < 100; i++) {
access();

__goblint_check(i == 8 * i + 0); //UNKNOWN!
__goblint_check(x_ptr == 8 * i + x_arr); //UNKNOWN!
__goblint_check(y_ptr == 4 * i + y_arr); //UNKNOWN!
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/77-lin2vareq/05-associative.c
Original file line number Diff line number Diff line change
Expand Up @@ -15,4 +15,4 @@ int main() {
}


//This test case checks the associative property
//This test case checks the associative property
2 changes: 1 addition & 1 deletion tests/regression/77-lin2vareq/07-commutative.c
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,4 @@ int main() {
return 0;
}

//This test case checks the commutative property.
//This test case checks the commutative property.
2 changes: 1 addition & 1 deletion tests/regression/77-lin2vareq/08-loop.c
Original file line number Diff line number Diff line change
Expand Up @@ -14,5 +14,5 @@ void main(void) {
k = k + 3;
}
__goblint_check(3 * i - k == 1); //UNKNOWN!

}
2 changes: 1 addition & 1 deletion tests/regression/77-lin2vareq/12-overflow.c
Original file line number Diff line number Diff line change
Expand Up @@ -20,4 +20,4 @@ int main() {
}

return 0;
}
}
2 changes: 1 addition & 1 deletion tests/regression/77-lin2vareq/13-bounds_guards_ov.c
Original file line number Diff line number Diff line change
Expand Up @@ -15,4 +15,4 @@ int main() {
__goblint_check(1);
}

}
}

0 comments on commit 5f56257

Please sign in to comment.