Project

General

Profile

Actions
Copy link

Feature #10910

open

Finalize support for verification of Harmony OS

Added by Evgeny Novikov over 2 years ago. Updated over 2 years ago.

Status:
New
Priority:
High
Assignee:
Evgeny Novikov
Category:
-
Target version:
-
Start date:
08/21/2021
Due date:
% Done:

0%

Estimated time:
(Total: 0.00 h)
Published in build:

Description

We added preliminary support for verification of Harmony OS in branch "harmonyos" ~half a year ago. Now its time to add this functionality to the master branch. Otherwise it will deprecate soon.

Subtasks 2 (2 open — 0 closed)

Bug #10911: Do not return anything from void functionsNewIlja Zakharov08/21/2021

Actions
Bug #10912: EMG does not generate separate threads for manually specified functionsNewIlja Zakharov08/23/2021

Actions

Related issues 1 (1 open — 0 closed)

Blocks Klever - Bug #10826: Klever uploads witnesses very slowNewEvgeny Novikov04/28/2021

Actions
Actions
Copy link
 #1

Updated by Evgeny Novikov over 2 years ago

I merged latest master to branch "harmonyos" in a new branch named "harmonyos-merge-master". Currently verification does not work. There is a bug in EMG or/and its specifications/settings (I will open a separate issue for this). Besides, Pavel will investigate why CPALockator reports Safe and does not find any data races.

Actions
Copy link
 #2

Updated by Evgeny Novikov over 2 years ago

  • Blocks Bug #10826: Klever uploads witnesses very slow added
Actions
Copy link
 #3

Updated by Evgeny Novikov over 2 years ago

  • Target version changed from 3.3 to 3.4
Actions
Copy link
 #4

Updated by Evgeny Novikov over 2 years ago

  • Target version changed from 3.4 to 3.5
Actions
Copy link
 #5

Updated by Evgeny Novikov over 2 years ago

  • Target version deleted (3.5)

There is no stakeholders for these issues. Let's do only those things that are really vital for somebody.

Actions
Copy link

Also available in: Atom PDF