File tree 6 files changed +40
-4
lines changed
6 files changed +40
-4
lines changed Original file line number Diff line number Diff line change
1
+ class t1
2
+ {
3
+ public:
4
+ t1 (int n) : value(n)
5
+ {
6
+ }
7
+
8
+ int value;
9
+ int operator [](int n)
10
+ {
11
+ return n * value;
12
+ }
13
+ };
14
+
15
+ int operator +(t1 left, int right)
16
+ {
17
+ return left.value + right;
18
+ }
19
+
20
+ int main ()
21
+ {
22
+ t1 t (10 );
23
+ int t_1 = t + 5 ;
24
+ int t_2 = t[5 ];
25
+ __CPROVER_assert (t_1 == 15 , " " );
26
+ __CPROVER_assert (t_2 == 50 , " " );
27
+ return 0 ;
28
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.cpp
3
+
4
+ ^EXIT=0$
5
+ ^SIGNAL=0$
6
+ --
7
+ ^warning: ignoring
8
+ ^CONVERSION ERROR$
Original file line number Diff line number Diff line change 1
- KNOWNBUG
1
+ CORE
2
2
main.cpp
3
3
4
4
^EXIT=0$
Original file line number Diff line number Diff line change 1
- KNOWNBUG
1
+ CORE
2
2
main.cpp
3
3
4
4
^EXIT=0$
Original file line number Diff line number Diff line change 1
- KNOWNBUG
1
+ CORE
2
2
main.cpp
3
3
4
4
^EXIT=0$
Original file line number Diff line number Diff line change @@ -3402,7 +3402,7 @@ bool Parser::rOperatorName(irept &name)
3402
3402
case ' <' :
3403
3403
case ' >' :
3404
3404
case ' ,' :
3405
- operator_id= irep_idt ( std::string (static_cast <char >(t), 1 ));
3405
+ operator_id = std::string (1 , static_cast <char >(t));
3406
3406
break ;
3407
3407
3408
3408
case TOK_MULTASSIGN: operator_id=" *=" ; break ;
You can’t perform that action at this time.
0 commit comments