fixed the expected testes

model-checking · Nov 20, 2024 · 3ec593d · 3ec593d
1 parent 997db12
commit 3ec593d
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 15 deletions.
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
@@ -213,7 +213,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         CharonScalarValue::from_bits(int_ty, discr_val)
     }
 
-    fn generic_params_from_adtdef(&self, adtdef: AdtDef) -> CharonGenericParams {
+    fn generic_params_from_adtdef(&mut self, adtdef: AdtDef) -> CharonGenericParams {
         let genvec = match adtdef.ty().kind() {
             TyKind::RigidTy(RigidTy::Adt(_, genarg)) => genarg.0,
             _ => panic!("generic_params_from_adtdef: not an adtdef"),
@@ -248,7 +248,21 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 GenericArgKind::Const(tc) => {
                     match tc.kind() {
                         TyConstKind::Param(paramtc) => {
-                            let lit_ty = CharonLiteralTy::Integer(CharonIntegerTy::I32); //TO BE CHECKED, PARAMENV
+                            //let lit_ty = CharonLiteralTy::Integer(CharonIntegerTy::I32); //TO BE CHECKED, PARAMENV
+                            let def_id_internal =
+                                rustc_internal::internal(self.tcx, adtdef.def_id());
+                            let paramenv = self.tcx.param_env(def_id_internal);
+                            let pc_internal = rustc_middle::ty::ParamConst {
+                                index: paramtc.index,
+                                name: rustc_span::Symbol::intern(&paramtc.name),
+                            };
+                            let ty_internal = pc_internal.find_ty_from_env(paramenv);
+                            let ty_stable = rustc_internal::stable(ty_internal);
+                            let trans_ty = self.translate_ty(ty_stable);
+                            let lit_ty = match trans_ty.kind() {
+                                CharonTyKind::Literal(lit) => lit.clone(),
+                                _ => panic!("generic_params_from_adtdef: not a literal type"),
+                            };
                             let c_constgeneric = CharonConstGenericVar {
                                 index: CharonConstGenericVarId::from_usize(paramtc.index as usize),
                                 name: paramtc.name.clone(),

diff --git a/tests/expected/llbc/enum_test/expected b/tests/expected/llbc/enum_test/expected
@@ -29,7 +29,7 @@ fn test::main()
     let i@2: i32; // local
 
     e@1 := test::MyEnum::A { 0: const (1 : i32) }
-    i@2 := @Fun1(move (e@1))
+    i@2 := @Fun0(move (e@1))
     drop i@2
     @0 := ()
     return

diff --git a/tests/expected/llbc/projection_test/expected b/tests/expected/llbc/projection_test/expected
@@ -5,22 +5,22 @@ struct test::MyStruct =
 }
 
 enum test::MyEnum0 =
-|  A(0: @Adt0, 1: i32)
+|  A(0: @Adt1, 1: i32)
 |  B()
 
 
 enum test::MyEnum =
-|  A(0: @Adt0, 1: @Adt2)
+|  A(0: @Adt1, 1: @Adt2)
 |  B(0: (i32, i32))
 
 
-fn test::enum_match(@1: @Adt1) -> i32
+fn test::enum_match(@1: @Adt0) -> i32
 {
     let @0: i32; // return
-    let e@1: @Adt1; // arg #1
-    let s@2: @Adt0; // local
+    let e@1: @Adt0; // arg #1
+    let s@2: @Adt1; // local
     let e0@3: @Adt2; // local
-    let s1@4: @Adt0; // local
+    let s1@4: @Adt1; // local
     let b@5: i32; // local
     let @6: i32; // anonymous local
     let @7: i32; // anonymous local
@@ -66,18 +66,18 @@ fn test::enum_match(@1: @Adt1) -> i32
 fn test::main()
 {
     let @0: (); // return
-    let s@1: @Adt0; // local
-    let s0@2: @Adt0; // local
-    let e@3: @Adt1; // local
+    let s@1: @Adt1; // local
+    let s0@2: @Adt1; // local
+    let e@3: @Adt0; // local
     let @4: @Adt2; // anonymous local
     let i@5: i32; // local
 
-    s@1 := @Adt0 { a: const (1 : i32), b: const (2 : i32) }
-    s0@2 := @Adt0 { a: const (1 : i32), b: const (2 : i32) }
+    s@1 := @Adt1 { a: const (1 : i32), b: const (2 : i32) }
+    s0@2 := @Adt1 { a: const (1 : i32), b: const (2 : i32) }
     @4 := test::MyEnum0::A { 0: move (s0@2), 1: const (1 : i32) }
     e@3 := test::MyEnum::A { 0: move (s@1), 1: move (@4) }
     drop @4
-    i@5 := @Fun1(move (e@3))
+    i@5 := @Fun0(move (e@3))
     drop i@5
     @0 := ()
     return