Skip to content

Goto-transcoder action - #236

Merged
feliperodri merged 13 commits into
model-checking:mainfrom
rafaelsamenezes:main
Jan 29, 2025
Merged

Goto-transcoder action#236
feliperodri merged 13 commits into
model-checking:mainfrom
rafaelsamenezes:main

Conversation

@rafaelsamenezes

@rafaelsamenezesrafaelsamenezes commented Jan 17, 2025

Copy link
Copy Markdown

Resolves#108

This PR enables the use of goto-transcoder for the following contracts:

core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_u8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_mul_i8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_mul_u8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shl_i8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shl_u8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shr_i8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shr_u8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_sub_i8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_sub_u8.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i32.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i64.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u32.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u64.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_mul_i16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_mul_u16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i32.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i64.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u32.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u64.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i32.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i64.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u32.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u64.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i32.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i64.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u16.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u32.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u64.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_add_i128.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_add_u128.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shl_i128.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shl_u128.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shr_i128.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shr_u128.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_sub_i128.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_sub_u128.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_add_isize.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_add_usize.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shl_isize.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shl_usize.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shr_isize.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shr_usize.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_sub_isize.out
core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_sub_usize.out

The version of ESBMC used contains the following solvers:

  • Boolector (default)
  • Z3

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

fixes on action script
removed checkout subfolder
fixed typo
@rafaelsamenezes
rafaelsamenezes requested a review from a team as a code ownerJanuary 17, 2025 14:24

@celinvalcelinval left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good. Thanks

Comment threadscripts/run-goto-transcoder.sh
Comment threadscripts/run-goto-transcoder.sh Outdated
Comment threadscripts/run-goto-transcoder.sh Outdated
Comment threadscripts/run-goto-transcoder.sh
Comment threadscripts/run-goto-transcoder.sh
Comment thread.github/workflows/goto-transcoder.yml
@feliperodrifeliperodri added the Tool Application Used to tag tool application label Jan 22, 2025
Comment threadrust-toolchain.toml Outdated
Comment threadscripts/run-goto-transcoder.sh
Comment thread.github/workflows/goto-transcoder.yml Outdated
Comment threadscripts/run-goto-transcoder.sh
@feliperodri
feliperodri added this pull request to the merge queueJan 29, 2025
Merged via the queue into model-checking:main with commit 566cd13Jan 29, 2025
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Tool ApplicationUsed to tag tool application

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Tool proposal: GOTO Transcoder (ESBMC)

4 participants

@rafaelsamenezes@tautschnig@feliperodri@celinval