To fix:

• ForeignItems/main.rs
  • Static extern variables not declared
• SizeAndAlignOfDst/main_fail.rs
  • __CPROVER_atomic_begin and __CPROVER_atomic_end
  • error: use of undeclared identifier '_ZN3std9panicking11panic_count18GLOBAL_PANIC_COUNT17hbb0e4a14d9617703E'
• Waiting on CBMC fix
  • Parameter name matches local var
    • VolatileIntrinsics/main.rs
      • default is a keyword
      • Something to do with pointers
    • Strings/fixme_boxed_str.rs
      • Something to do with pointers
    • FatPointers/boxmuttrait.rs
      • byte_extract_little_endian defined wrong
      • Issue with parameter name matching local variable name.
    • Cast/from_be_bytes.rs
      • Something to do with overlapping parameter and local variable names?
    • Intrinsics/fixme_catch_unwind.rs
      • Something to do with overlapping parameter and local variable names?
    • Vectors/fixme_main.rs
  • Irep
    • BitManipulation/Stable/fixme_main_fail.rs
      • error: implicit declaration of function 'irep' is invalid in C99
    • BitManipulation/Unstable/Rotate/main.rs
      • error: implicit declaration of function 'irep' is invalid in C99
    • Vectors/fixme_main.rs
• Done
  • SIMD/Operators/main.rs
    • error: assigning to 'long *' from incompatible type '__attribute__((__vector_size__(2 * sizeof(long)))) long'
    • error: address of vector element requested
  • DynTrait/*
    • error: indirection requires pointer operand ('struct _closure_DynTrait_boxed_closure_fail_fixme_rs_14_44__16_6_' invalid)
    • (This is caused by a bug which is currently being patched.)
  • CodegenConstValue/u128.rs
    • error: integer literal is too large to be represented in any integer type
  • PointerOffset/*
    • error: implicit declaration of function 'POINTER_OBJECT' is invalid in C99
  • SizeAndAlignOfDst/main.rs
    • __CPROVER_atomic_begin and __CPROVER_atomic_end
  • Atomics/*
    • __CPROVER_atomic_begin and __CPROVER_atomic_end
  • Cast/cast_abstract_args_to_concrete.rs
    • powi and powif not defined
  • CopyIntrinsics/main.rs
    • default is a keyword
    • Something to do with pointers
  • Asm/main_fixme.rs
    • No default value for type empty

Simplified version of error: assigning to 'long *' from incompatible type '__attribute__((__vector_size__(2 * sizeof(long)))) long'

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
#![feature(repr_simd)]

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(PartialEq)]
pub struct i64x2(i64, i64);

fn main() {
    assert!(i64x2(0, 0) == i64x2(0, 0));
}

Changes:

• Normalizing identifiers

  • Replace non-alphanumeric + "" + "$" with ""
  • Add "_" before name if starts with number
  • Add "_" to key words
  • If overlapping output names, add "_"

• Transform names

  • Symbol name
  • Parameters
  • Member access to structs/unions
  • Symbol expr
  • Structs
    • Struct name
    • Struct component
    • Struct type
  • Unions
    • Union name
    • Union field
    • Union component
    • Union type
  • Goto/labels

• Replacements

  • Big nums
    • If a constant goes above u64::MAX, break into (a * u64::MAX + b)
  • Bin ops
    • Replace lhs ==> rhs with !lhs || rhs
  • Vector indexing
    • Cast vector to array, and then index
  • Replace main with main_ so we can create main with int return type

• Nondet

  • Replace nondet calls with calls to custom non_det functions with default return values
    • Except padding fields, since they are ignored, and ignored nondets are not genned in --dump-c
  • Fill in missing extern functions with calls to nondet

• C library

  • Manually define some CPROVER stuff